Model: | majority v.1 (CTMC) |
Parameter(s) | T = 2100 |
Property: | change_state (prob-reach-time-bounded) |
mcsta/modest mcsta majority.jani -E T=2100 --props change_state -O out.txt Minimal --unsafe --es -S Memory --width 0 --p0 --p1
Walltime: | 0.21553444862365723s |
Return code: | 0 |
Note(s): | Unable to obtain tool result. |
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c. The maximum half-width of the bounds intervals computed by sound numeric methods must be positive. Run modest mcsta --help to show usage information.